T:Type, X:MaInterface(T), es:ES, e:E.
(ma-in-interface(es;X;e))
 ((loc(e)  ma-interface-locs(X)) & (kind(e)  ma-interface-dom(X;loc(e)))) 

latex

Definitions

x:A. B(x), MaInterface(T), b, ma-in-interface(es;X;e), ma-interface-locs(I), ma-interface-dom(I;i), p  q, t  T, x. t(x), , P  Q, tt, if b then t else f fi , ff, t.2, a:A fp B(a), Knd, Top, P  Q, P & Q, P  Q, A c B, , x(s), Unit, (x  l), x:A. B(x), A, False, , fpf-domain(f)

Lemmas

fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, es-loc wf, bool wf, eqtt to assert, member-fpf-domain, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, es-E wf, event system wf, Id wf, fpf-ap wf, IdLnk wf, subtype rel product, l member wf, subtype rel list, subtype rel set, subtype rel function, subtype-set-hasloc, member-fpf-dom, fpf-domain wf, false wf